Asynchronous programming is a ubiquitous systems programming idiom to manageconcurrent interactions with the environment. In this style, instead of waitingfor time-consuming operations to complete, the programmer makes a non-blockingcall to the operation and posts a callback task to a task buffer that isexecuted later when the time-consuming operation completes. A co-operativescheduler mediates the interaction by picking and executing callback tasks fromthe task buffer to completion (and these callbacks can post further callbacksto be executed later). Writing correct asynchronous programs is hard becausethe use of callbacks, while efficient, obscures program control flow. We provide a formal model underlying asynchronous programs and studyverification problems for this model. We show that the safety verificationproblem for finite-data asynchronous programs is expspace-complete. We showthat liveness verification for finite-data asynchronous programs is decidableand polynomial-time equivalent to Petri Net reachability. Decidability is notobvious, since even if the data is finite-state, asynchronous programsconstitute infinite-state transition systems: both the program stack and thetask buffer of pending asynchronous calls can be potentially unbounded. Our main technical construction is a polynomial-time semantics-preservingreduction from asynchronous programs to Petri Nets and conversely. Thereduction allows the use of algorithmic techniques on Petri Nets to theverification of asynchronous programs. We also study several extensions to the basic models of asynchronous programsthat are inspired by additional capabilities provided by implementations ofasynchronous libraries, and classify the decidability and undecidability ofverification questions on these extensions.
展开▼
